Conclusions in [Zantema - RTA'97]

Summary: ExConc_Zan97

• CS-TRS format
• OBJ format
• Negative results:
  1. Zantema's transformation (non-terminating)
• Positive results:
  1. Lucas' transformation (Polynomials @ MuTerm)
  2. Ferreira and Ribeiro's transformation (Polynomials @ MuTerm)
  3. Giesl and Middeldorp's transformation (Polynomials @ MuTerm)
  4. CSRPO
  5. Polynomial interpretation (MuTerm)
  6. CSDP

CS-TRS ExConc_Zan97 (file ExConc_Zan97.csr)

Functions:  f g h

Constructors:  g h

Variables:  X

Arities: 

ar(f) = 1
ar(g) = 1
ar(h) = 1

Replacement map: 

µ(f)={1}
µ(g)={}
µ(h)={1}

Rules:  (file ExConc_Zan97) 

f(X) -> g(h(f(X)))

The CS-TRS in OBJ format (file ExConc_Zan97.obj):

obj ExIntrod_Zan97 is
  sort S .
  op fact : S -> S .
  op if : S S S -> S [strat (1 0)] .
  op zero : S -> S .
  op s : S -> S .
  op 0 : -> S .
  op prod : S S -> S .
  op p : S -> S .
  op add : S S -> S .
  op true : -> S .
  op false : -> S .
  vars X Y : S .
  eq fact(X) = if(zero(X),s(0),prod(X,fact(p(X)))) .
  eq add(0,X) = X .
  eq add(s(X),Y) = s(add(X,Y)) .
  eq prod(0,X) = 0 .
  eq prod(s(X),Y) = add(Y,prod(X,Y)) .
  eq if(true,X,Y) = X .
  eq if(false,X,Y) = Y .
  eq zero(0) = true .
  eq zero(s(X)) = false .
  eq p(s(X)) = X .
endo

Negative results

1. The µ-termination of ExConc_Zan97 cannot be proved by using Zantema's transformation. The TRS ExConc_Zan97_Z:

       f(X) -> g(n__h(f(X)))
       h(X) -> n__h(X)
       activate(n__h(X)) -> h(X)
       activate(X) -> X
       

   is not terminating (due to the first rule).

Positive results

1. ExConc_Zan97 can be proved µ-terminating by using Lucas' transformation. The TRS ExConc_Zan97_L:

       f(X) -> g
       

   can be proved terminating (use MuTerm).
2. The µ-termination of ExConc_Zan97 can also be proved by using Ferreira and Ribeiro's transformation (use MuTerm).
3. The µ-termination of ExConc_Zan97 can also be proved by using Giesl and Middeldorp's transformation: the TRS ExConc_Zan97_GM:

       a__f(X) -> g(h(f(X)))
       mark(f(X)) -> a__f(mark(X))
       mark(g(X)) -> g(X)
       mark(h(X)) -> h(mark(X))
       a__f(X) -> f(X)
       

   can be proved terminating (use MuTerm).
4. The µ-termination of ExConc_Zan97 is proved in [BLR02, Example 6] by using CSRPO and automatically using ( MuTerm):.
5. The µ-termination of ExConc_Zan97 can also be proved by using a polynomial interpretation (computed by MuTerm):

       Proof of termination for CS-TRS  ExConc_Zan97:
   
       [f](X) = X + 1
       [g](X) = 0
       [h](X) = X
       

6. The µ-termination of ExConc_Zan97 is proved with CSDP (computed with MuTerm).